Listar por autor 

Listar por autor "Ruiz Reina, José Luis"                

Mostrando ítems 1-20 de 32

    • Ponencia
      Icon

      A Formal Proof of Dickson’s Lemma in ACL2 

      Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (Springer, 2003)
      Dickson’s Lemma is the main result needed to prove the termination of Buchberger’s algorithm for computing Gr¨obner basis ...
    • Ponencia
      Icon

      A Formally Verified Prover for the ALC Description Logic 

      Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Springer, 2007)
      The Ontology Web Language (OWL) is a language used for the Semantic Web. OWL is based on Description Logics (DLs), a ...
    • Ponencia
      Icon

      A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory. 

      Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (University of Texas, 2002)
      In some cases, when we develop a formal theory in ACL2, it would be desirable that the definitions and theorems of the ...
    • Ponencia
      Icon

      A Theory About First-Order Terms in ACL2 

      Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (University of Texas, 2002)
      We describe the development in ACL2 of a library of results about first-order terms. In particular, we present the ...
    • Artículo
      Icon

      A verified Common Lisp implementation of Buchberger's algorithm in ACL2 

      Medina Bulo, Inmaculada; Palomo Lozano, Francisco; Ruiz Reina, José Luis (Elsevier, 2010)
      In this article, we present the formal verification of a Common Lisp implementation of Buchberger's algorithm for ...
    • Ponencia
      Icon

      ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System 

      Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Springer, 2009)
      Kenzo is a Computer Algebra system devoted to Algebraic Topology, and written in the Common Lisp programming language. ...
    • Ponencia
      Icon

      Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials 

      Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Springer, 2011)
      In this paper we present a complete formalization, using the ACL2 theorem prover, of the Normalization Theorem, a result ...
    • Ponencia
      Icon

      Certified Symbolic Manipulation: Bivariate Simplicial Polynomials 

      Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (ACM, 2013)
      Certified symbolic manipulation is an emerging new field where programs are accompanied by certificates that, suitably ...
    • Artículo
      Icon

      Constructing Formally Verified Reasoners for the ALC Description Logic 

      Hidalgo Doblado, María José; Alonso Jiménez, José Antonio; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Elsevier, 2008)
      Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. ...
    • Libro
      Icon

      Curso Práctico de Teoría de Conjuntos 

      Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Pérez Jiménez, Mario de Jesús; Ruiz Reina, José Luis (Ediciones La Ñ, 1998)
      Todos los que hemos impartido tópicos diversos relativos a la Teoría de Conjuntos, en primer o segundo ciclo universitario, ...
    • Artículo
      Icon

      Efficient execution in an automated reasoning environment 

      Greve, David A.; Kaufmann, Matt; Manolios, Panagiotis; Moore, J. Strother; Ray, Sandip; Ruiz Reina, José Luis; Sumners, Rob; Vroon, Daron; Wilding, Matthew (Cambridge University Press, 2008)
      We describe a method that permits the user of a mechanized mathematical logic to write elegant logical definitions while ...
    • Artículo
      Icon

      Formal Correctness of a Quadratic Unification Algorithm 

      Ruiz Reina, José Luis; Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José (Springer, 2006)
      We present a case study using ACL2 [5] to verify a non-trivial algorithm that uses efficient data structures. The algorithm ...
    • Artículo
      Icon

      Formal proofs about rewriting using ACL2 

      Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (Springer, 2002)
      We present an application of the ACL2 theorem prover to reason about rewrite systems theory. We describe the formalization ...
    • Ponencia
      Icon

      Formal Reasoning about Efficient Data Structures: A Case Study in ACL2 

      Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (Springer, 2003)
      We describe in this paper the formal verification, using the ACL2 system, of a syntactic unification algorithm where terms ...
    • Artículo
      Icon

      Formal verification of a generic framework to synthesize SAT-provers 

      Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (Springer, 2004)
      We present in this paper an application of the ACL2 system to generate and reason about propositional satis ability ...
    • Ponencia
      Icon

      Formal Verification of Molecular Computational Models in ACL2: A Case Study 

      Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (Springer, 2003)
      Theorem proving is a classical AI problem with a broad range of applications. Since its complexity is exponential in the ...
    • Artículo
      Icon

      Formalization of a normalization theorem in simplicial topology 

      Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Springer, 2012)
      In this paper we present a complete formalization of the Normalization Theorem, a result in Algebraic Simplicial Topology ...
    • Ponencia
      Icon

      Formalizing Rewriting in the ACL2 Theorem Prover 

      Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (Springer, 2000)
      We present an application of the ACL2 theorem prover to formalize and reason about rewrite systems theory. This can be ...
    • Artículo
      Icon

      Formally Verified Tableau-Based Reasoners for a Description Logic 

      Hidalgo Doblado, María José; Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Springer, 2014)
      Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. One ...
    • Ponencia
      Icon

      Multiset Relations: A Tool for Proving Termination 

      Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (University of Texas, 2000)